Nuprl Definition : triggersGlue 11,40

triggersGlue(Altgdsconds)
== ([Rsframe(l;tg;fpf-domain(conds)); 

== ([xfpf-domain(conds).Rsends(ds;x;conds(x).1;l;if isrcvl(l;x)
== ([then tg : A  tag(x) : conds(x).1
== ([else tg : A
== ([fi ;[<tg
== ([fi ;[s,v. if can-apply(p.let s,v = p in (conds(x).2)(s,v);<sv>)
== ([fi ;[, then [do-apply(p.let s,v = p in (conds(x).2)(s,v);<sv>)]
== ([fi ;[, else []
== ([fi ;[, fi 
== ([fi ;[>])]) 
latex



clarification:

triggersGlue(Altgdsconds)
== ([Rsframe(l;tg;fpf-domain(conds)) / 
== ([[xfpf-domain(conds).Rsends(ds;x;condsKindDeq(x).1;l;if isrcvl(l;x)
== ([[then fpf-join(IdDeq;tg : A;tag(x) : condsKindDeq(x).1)
== ([[else tg : A
== ([[fi ;[<tg
== ([[fi ;[s,v. if can-apply(p.let s,v = p in (condsKindDeq(x).2)(s,v);<sv>)
== ([[fi ;[, then [do-apply(p.let s,v = p in (condsKindDeq(x).2)(s,v);<sv>) / []]
== ([[fi ;[, else []
== ([[fi ;[, fi 
== ([[fi ;[> / 
== ([[fi ;[[]]) / 
== ([[[]]]) 
latex


Definitions(L), Rsframe(lnk;tag;L), xL.R(x), fpf-domain(f), Rsends(ds;knd;T;l;dt;g), isrcvl(l;k), f  g, IdDeq, tag(k), t.1, x : v, if b then t else f fi , can-apply(f;x), [car / cdr], do-apply(f;x), x.A(x), let x,y = A in B(x;y), f(a), t.2, f(x), KindDeq, <ab>, []

origin